Merge branch 'master' into fix-makefile

Author: gares

AUTHORS.md

@@ -1,7 +1,8 @@
 Copyright (C) 2020
 
 - Cyril Cohen (Inria)
+- Pierre Roux (Onera)
 - Kazuhiko Sakaguchi (University of Tsukuba)
 - Enrico Tassi (Inria)
 
-This software is released under the terms of the MIT license, see LICENSE file.
+This software is released under the terms of the MIT license, see LICENSE file.

HB/builders.elpi

@@ -54,9 +54,6 @@ builders.end :- std.do! [
   acc-clauses current Clauses,
   acc-clauses current ExportClausesFiltered,
 
-  % Clauses => ExportClausesFiltered => current-mode no-builder =>
-  %   instance.declare-factory-sort-factory GR,
-
   log.coq.env.end-module-name Name Exports,
   log.coq.env.end-module-name ModName _,
   export.module {calc (ModName ^ "." ^ Name)} Exports,

HB/factory.elpi

@@ -294,8 +294,6 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
   @global! => log.coq.arguments.set-implicit GRK [[maximal|Implicits]],
   % @global! => log.coq.coercion.declare FactorySortCoe,
 
-  % NewClauses => instance.declare-factory-sort-deps (indt R),
-
   log.coq.env.end-module-name "Exports" Exports,
   log.coq.env.end-module-name Module _,
 
@@ -366,8 +364,6 @@ declare-factory-alias MixinSrcClauses SectionCanonicalInstance
   acc-clauses current NewClauses,
   %@global! => log.coq.coercion.declare FactorySortCoe,
 
-  % NewClauses => instance.declare-factory-sort-deps (const C),
-
   log.coq.env.end-module-name "Exports" Exports,
   log.coq.env.end-module-name Module _,
 

HB/instance.elpi

@@ -191,72 +191,6 @@ decl-const-in-struct Name S STy CS:- std.do![
   if-verbose (coq.say {header} "structure instance" Name "declared"),
 ].
 
-
-pred declare-factory-sort-deps i:gref.
-declare-factory-sort-deps  GR :- std.do! [
-  if-verbose (coq.say {header} "required instances on factory sort for" GR),
-  Name is "SortInstances" ^ {std.any->string {new_int}},
-  log.coq.env.begin-module Name none,
-  log.coq.env.begin-section Name,
-  mk-factory-sort-deps GR CSL,
-  log.coq.env.end-section-name Name,
-  log.coq.env.end-module-name Name _,
-  std.forall CSL (x\ sigma CS\ x = pr _ CS, log.coq.CS.declare-instance CS)
-].
-
-pred declare-factory-sort-factory i:gref.
-declare-factory-sort-factory GR :- std.do! [
-  if-verbose (coq.say {header} "required instances on factory sort for" GR),
-  Name is "SortInstances" ^ {std.any->string {new_int}},
-  log.coq.env.begin-module Name none,
-  log.coq.env.begin-section Name,
-  mk-factory-sort-factory GR CFL CSL,
-  log.coq.env.end-section-name Name,
-  log.coq.env.end-module-name Name _,
-  std.forall {std.append CFL CSL} (x\ sigma CS\ x = pr _ CS, log.coq.CS.declare-instance CS)
-].
-
-pred context.declare i:factories, o:mixins, o:list term, o:term, o:list prop, o:list constant.
-
-pred mk-factory-sort-deps i:gref, o:list (pair id constant).
-mk-factory-sort-deps AliasGR CSL :- std.do! [
-  std.assert-ok! (factory-alias->gref AliasGR GR) "HB: mk-factory-sort-deps",
-  gref-deps GR MLwPRaw,
-  context.declare MLwPRaw MLwP SortParams SortKey SortMSL _,
-  SortMSL => synthesis.infer-all-gref-deps SortParams SortKey GR FSort,
-  log.coq.env.add-section-variable-noimplicits "f" FSort CF,
-  GCF = global (const CF),
-  factory-sort (coercion GRFSort _ GR _),
-  SortMSL => synthesis.infer-all-gref-deps SortParams SortKey GRFSort KSort,
-  coq.mk-app KSort [GCF] KFSortEta,
-  list-w-params_list MLwP ML,
-  std.length ML NMLArgs,
-  coq.mk-n-holes NMLArgs SortMLHoles,
-  std.append {std.append SortParams [SortKey|SortMLHoles]} [GCF] KFSortArgs,
-  coq.mk-app (global GRFSort) KFSortArgs KFSort,
-  std.assert-ok! (coq.unify-eq KFSortEta KFSort) "HB: KRSort not an app",
-  std.map SortMSL
-    (c\ o\ sigma m t\ c = mixin-src _ m t, o = mixin-src KFSort m t)
-    KFSortMSL,
-  KFSortMSL =>
-    synthesis.under-mixin-src-from-factory.do! KFSort GCF
-      [declare-all KFSort {findall-classes-for ML} CSL]
-].
-
-pred mk-factory-sort-factory i:gref, o:list (pair id constant), o:list (pair id constant).
-mk-factory-sort-factory AliasGR CFL CSL :- std.do! [
-  std.assert-ok! (factory-alias->gref AliasGR GR) "HB",
-  gref-deps GR MLwPRaw,
-  context.declare MLwPRaw MLwP SortParams SortKey SortMSL _,
-  SortMSL => synthesis.infer-all-gref-deps SortParams SortKey GR FSort,
-  log.coq.env.add-section-variable-noimplicits "f" FSort CF,
-  std.length {list-w-params_list MLwP} NMLArgs,
-  coq.mk-n-holes NMLArgs SortMLHoles,
-  GCF = global (const CF),
-  coq.mk-app (global GR) {std.append SortParams [GCF|SortMLHoles]} FGCF,
-  declare-const "_" GCF (arity FGCF) CFL CSL
-].
-
 % create instances for all possible combinations of types and structure compatible 
 pred saturate-instances i:cs-pattern.
 saturate-instances Filter :- std.do! [

Makefile

@@ -110,8 +110,8 @@ this-config:: __always__
 			echo '*****************************************************************';\
 			echo 'old coq version detected, double check the diff before committing';\
 			echo '*****************************************************************';\
-			sed -i.bak `find . -name \*.v` -e 's/From Corelib/From Coq/' ; \
-			sed -i.bak `find . -name \*.v` -e 's/IntDef/ZArith/' ; \
+			sed -i.bak -e 's/From Corelib/From Coq/' `find . -name \*.v` ; \
+			sed -i.bak -e 's/IntDef/ZArith/' `find . -name \*.v` ; \
 		fi;\
 	fi