]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_tactics/nTacStatus.ml
nasty change in the lexer/parser:
[helm.git] / helm / software / components / ng_tactics / nTacStatus.ml
index 413afbef08247ee86e515a95949d07b9f4318c6d..a2847a410061089440699f1612b412555f652b50 100644 (file)
@@ -340,5 +340,5 @@ let mk_cic_term c t = None,c,t ;;
 let apply_subst status ctx t =
  let status, (name,_,t) = relocate status ctx t in
  let _,_,_,subst,_ = status.pstatus in
-  status, (name, ctx, NCicUntrusted.apply_subst subst t)
+  status, (name, ctx, NCicUntrusted.apply_subst subst ctx t)
 ;;