From e8ef565dadd110329f806fa3c281055fcd807440 Mon Sep 17 00:00:00 2001 From: lmamane Date: Fri, 22 Feb 2008 13:39:13 +0000 Subject: Merge with lmamane's private branch: - New vernac command "Delete" - New vernac command "Undo To" - Added a few hooks used by new contrib/interface - Beta/incomplete version of dependency generation and dumping git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10580 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/funind/rawterm_to_relation.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'contrib/funind') diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml index e6b3ba3ec..7d0d134c5 100644 --- a/contrib/funind/rawterm_to_relation.ml +++ b/contrib/funind/rawterm_to_relation.ml @@ -446,7 +446,7 @@ let rec pattern_to_term_and_type env typ = function let patl_as_term = List.map2 (pattern_to_term_and_type env) (List.rev cs_args_types) patternl in - mkRApp(mkRRef(Libnames.ConstructRef constr), + mkRApp(mkRRef(ConstructRef constr), implicit_args@patl_as_term ) -- cgit v1.2.3