the trie indexes terms up to 10 nested applications and skips applications with more...

[helm.git] / helm / software / components / ng_refiner / nCicMetaSubst.ml

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index bdd0adfe014f3acba18eab6a1270c55527d012d5..421194abdb02b3a4431149b995e6b7493e104248 100644 (file)
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -207,11 +207,18 @@ and restrict metasenv subst i restrictions =
 ;;
 
 let rec flexible_arg context subst = function 
-  | NCic.Meta (i,_) | NCic.Appl (NCic.Meta (i,_) :: _)-> 
+  | NCic.Meta (i,_) ->
       (try 
         let _,_,t,_ = List.assoc i subst in
         flexible_arg context subst t
       with Not_found -> true)
+  | NCic.Appl (NCic.Meta (i,_) :: args)-> 
+      (try 
+        let _,_,t,_ = List.assoc i subst in
+        flexible_arg context subst 
+          (NCicReduction.head_beta_reduce ~delta:max_int 
+            (NCic.Appl (t :: args)))
+      with Not_found -> true)
    (* this is a cheap whd, it only performs zeta-reduction.
     * 
     * it works when the **omissis** disambiguation algorithm
@@ -463,7 +470,7 @@ let mk_meta ?(attrs=[]) metasenv context ty =
     menv_entry :: metasenv, n, NCic.Meta (n, (0,NCic.Irl len)), ty
   | `Sort ->
     let ty = NCic.Implicit (`Typeof n) in
-    mk_meta (tyof attrs) n metasenv [] (`WithType ty)
+    mk_meta (`IsSort::tyof attrs) n metasenv [] (`WithType ty)
   | `Type ->
     let metasenv, _, ty, _ = 
       mk_meta (tyof attrs) (newmeta ()) metasenv context `Sort in