unify left args of inductive types with left argus of constructors. this allows

to put ? in every left arg of every constructor of an inductive type.

diff --git a/helm/software/components/ng_refiner/.depend b/helm/software/components/ng_refiner/.depend
index d3a179400fd094589a1aa1e10e5ea5968655f6b5..da0ab80fc1102419bb4d0668c1e3cd21e0daba14 100644 (file)
--- a/helm/software/components/ng_refiner/.depend
+++ b/helm/software/components/ng_refiner/.depend
@@ -22,7 +22,7 @@ nCicRefineUtil.cmo: nCicMetaSubst.cmi nCicRefineUtil.cmi
 nCicRefineUtil.cmx: nCicMetaSubst.cmx nCicRefineUtil.cmi 
 nCicUnification.cmo: nCicUnifHint.cmi nCicMetaSubst.cmi nCicUnification.cmi 
 nCicUnification.cmx: nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi 
-nCicRefiner.cmo: nCicUnification.cmi nCicMetaSubst.cmi nCicCoercion.cmi \
-    nCicRefiner.cmi 
-nCicRefiner.cmx: nCicUnification.cmx nCicMetaSubst.cmx nCicCoercion.cmx \
-    nCicRefiner.cmi 
+nCicRefiner.cmo: nCicUnification.cmi nCicRefineUtil.cmi nCicMetaSubst.cmi \
+    nCicCoercion.cmi nCicRefiner.cmi 
+nCicRefiner.cmx: nCicUnification.cmx nCicRefineUtil.cmx nCicMetaSubst.cmx \
+    nCicCoercion.cmx nCicRefiner.cmi 

diff --git a/helm/software/components/ng_refiner/.depend.opt b/helm/software/components/ng_refiner/.depend.opt
index db7e5288428cc5c63f47f29ba31c99d41f9412d3..da0ab80fc1102419bb4d0668c1e3cd21e0daba14 100644 (file)
--- a/helm/software/components/ng_refiner/.depend.opt
+++ b/helm/software/components/ng_refiner/.depend.opt
@@ -3,6 +3,7 @@ nCicMetaSubst.cmi:
 nCicUnifHint.cmi: 
 nCicCoercion.cmi: nCicUnifHint.cmi 
 nRstatus.cmi: nCicCoercion.cmi 
+nCicRefineUtil.cmi: 
 nCicUnification.cmi: nRstatus.cmi 
 nCicRefiner.cmi: nRstatus.cmi 
 nDiscriminationTree.cmo: nDiscriminationTree.cmi 
@@ -17,9 +18,11 @@ nCicCoercion.cmx: nDiscriminationTree.cmx nCicUnifHint.cmx nCicMetaSubst.cmx \
     nCicCoercion.cmi 
 nRstatus.cmo: nCicCoercion.cmi nRstatus.cmi 
 nRstatus.cmx: nCicCoercion.cmx nRstatus.cmi 
+nCicRefineUtil.cmo: nCicMetaSubst.cmi nCicRefineUtil.cmi 
+nCicRefineUtil.cmx: nCicMetaSubst.cmx nCicRefineUtil.cmi 
 nCicUnification.cmo: nCicUnifHint.cmi nCicMetaSubst.cmi nCicUnification.cmi 
 nCicUnification.cmx: nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi 
-nCicRefiner.cmo: nCicUnification.cmi nCicMetaSubst.cmi nCicCoercion.cmi \
-    nCicRefiner.cmi 
-nCicRefiner.cmx: nCicUnification.cmx nCicMetaSubst.cmx nCicCoercion.cmx \
-    nCicRefiner.cmi 
+nCicRefiner.cmo: nCicUnification.cmi nCicRefineUtil.cmi nCicMetaSubst.cmi \
+    nCicCoercion.cmi nCicRefiner.cmi 
+nCicRefiner.cmx: nCicUnification.cmx nCicRefineUtil.cmx nCicMetaSubst.cmx \
+    nCicCoercion.cmx nCicRefiner.cmi 

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 8476119ad081c24489559e5e2e566ea0318f13bb..7833b9c4a202e55f8380f401f4c4e408cb15f156 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -1128,6 +1128,29 @@ let typeof_obj
                     metasenv,subst,item1::context
                 ) (metasenv,subst,tys) sx_context_ty_rev sx_context_te_rev
               with Invalid_argument "List.fold_left2" -> assert false in
+             let metasenv, subst =
+                let rec aux context (metasenv,subst) = function
+                  | NCic.Meta _ -> metasenv, subst
+                  | NCic.Implicit _ -> metasenv, subst
+                  | NCic.Appl (NCic.Rel i :: args) as t
+                      when i >= List.length context - len ->
+                      let lefts, _ = HExtlib.split_nth leftno args in
+                      let ctxlen = List.length context in
+                      let (metasenv, subst), _ = 
+                        List.fold_left
+                        (fun ((metasenv, subst),l) arg ->
+                          NCicUnification.unify rdb 
+                           ~test_eq_only:true metasenv subst context arg 
+                             (NCic.Rel (ctxlen - len - l)), l+1
+                          )
+                        ((metasenv, subst), 0) lefts
+                      in
+                      metasenv, subst
+                  | t -> NCicUtils.fold (fun e c -> e::c) context aux
+                  (metasenv,subst) t
+                in
+               aux context (metasenv,subst) te
+             in
              let con_sort= NCicTypeChecker.typeof ~subst ~metasenv context te in
               (match
                 NCicReduction.whd ~subst context con_sort,